\begin{tabbing}
approx\_sm(${\it es}$; ${\it In}$; ${\it Out}$; ${\it Cmd}$; ${\it isupdate}$; ${\it Rsp}$; ${\it Delta}$; $Q$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=${\it expl}$:es{-}E{-}interface(${\it es}$;${\it Out}$)$\rightarrow$(\{$e$:es{-}E{-}interface(${\it es}$;${\it In}$)$\mid$ $\uparrow$(${\it isupdate}$(${\it In}$($e$)))\}  List)\+
\\[0ex]((\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Out}$).\+
\\[0ex](\=$\forall$${\it e'}$:es{-}E{-}interface(${\it es}$;${\it In}$).\+
\\[0ex](${\it e'}$ $\in$ ${\it expl}$($e$) $\in$ es{-}E{-}interface(${\it es}$;${\it In}$)) $\Rightarrow$ es{-}causle(${\it es}$;${\it e'}$;$e$))
\-\\[0ex]\& (($\neg$is{-}query(${\it In}$;${\it isupdate}$;$e$)) $\Rightarrow$ ($\neg$($\uparrow$null(${\it expl}$($e$))))))
\-\\[0ex]\& (\=$\forall$$e_{1}$:es{-}E{-}interface(${\it es}$;${\it Out}$), $e_{2}$:es{-}E{-}interface(${\it es}$;${\it Out}$).\+
\\[0ex]${\it expl}$($e_{1}$) $\leq$ ${\it expl}$($e_{2}$) $\in$ es{-}E{-}interface(${\it es}$;${\it In}$) List
\\[0ex]$\vee$ ${\it expl}$($e_{2}$) $\leq$ ${\it expl}$($e_{1}$) $\in$ es{-}E{-}interface(${\it es}$;${\it In}$) List)
\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Out}$).\+
\\[0ex](is{-}query(${\it In}$;${\it isupdate}$;$e$) $\Rightarrow$ (${\it Out}$($e$) = $Q$(${\it In}$(${\it expl}$($e$)),${\it In}$($e$)) $\in$ ${\it Rsp}$))
\\[0ex]\& (($\neg$is{-}query(${\it In}$;${\it isupdate}$;$e$)) $\Rightarrow$ (${\it Out}$($e$) = ${\it Delta}$(${\it In}$(${\it expl}$($e$))) $\in$ ${\it Rsp}$))))
\-\-
\end{tabbing}